(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 1))
(let ((e4 2))
(let ((e5 (/ e4 (- e3))))
(let ((e6 (/ e3 (- e4))))
(let ((e7 (* e5 (- e3))))
(let ((e8 (* e3 e7)))
(let ((e9 (+ e7 e7)))
(let ((e10 (- e9 e6)))
(let ((e11 (* e9 e6)))
(let ((e12 (/ e3 e3)))
(let ((e13 (* e9 e8)))
(let ((e14 (+ e13 e9)))
(let ((e15 (* v0 e14)))
(let ((e16 (/ e3 (- e4))))
(let ((e17 (- e6)))
(let ((e18 (- e15 e7)))
(let ((e19 (/ e3 e4)))
(let ((e20 (- v1 e10)))
(let ((e21 (+ e9 v2)))
(let ((e22 (> v0 e5)))
(let ((e23 (> v2 e14)))
(let ((e24 (= e20 e6)))
(let ((e25 (<= e20 e13)))
(let ((e26 (<= e10 e16)))
(let ((e27 (>= e18 e21)))
(let ((e28 (= e7 e7)))
(let ((e29 (distinct v2 e14)))
(let ((e30 (= v0 v1)))
(let ((e31 (>= e7 e10)))
(let ((e32 (>= e9 e8)))
(let ((e33 (>= e20 e15)))
(let ((e34 (distinct e7 e6)))
(let ((e35 (= e10 e10)))
(let ((e36 (>= e15 e15)))
(let ((e37 (<= e15 e15)))
(let ((e38 (<= e10 v0)))
(let ((e39 (distinct e14 v2)))
(let ((e40 (> e9 v2)))
(let ((e41 (> v2 e15)))
(let ((e42 (>= e15 e8)))
(let ((e43 (>= e11 v2)))
(let ((e44 (distinct e8 e10)))
(let ((e45 (>= v1 e15)))
(let ((e46 (>= e18 e5)))
(let ((e47 (distinct e17 e12)))
(let ((e48 (>= e15 e11)))
(let ((e49 (>= v1 v2)))
(let ((e50 (< e18 e12)))
(let ((e51 (< e16 v0)))
(let ((e52 (< v2 e9)))
(let ((e53 (> e10 e11)))
(let ((e54 (< e8 e9)))
(let ((e55 (<= e13 e10)))
(let ((e56 (<= e17 e16)))
(let ((e57 (>= e12 e13)))
(let ((e58 (<= e5 e21)))
(let ((e59 (> e15 e19)))
(let ((e60 (>= e5 e14)))
(let ((e61 (<= v0 e5)))
(let ((e62 (< e10 e19)))
(let ((e63 (= v1 e9)))
(let ((e64 (< v0 e21)))
(let ((e65 (< e10 e15)))
(let ((e66 (> e11 e18)))
(let ((e67 (= e17 e14)))
(let ((e68 (> e16 v1)))
(let ((e69 (= e8 v0)))
(let ((e70 (>= e18 e13)))
(let ((e71 (<= e18 e19)))
(let ((e72 (< e15 e11)))
(let ((e73 (distinct e8 e14)))
(let ((e74 (distinct e10 v2)))
(let ((e75 (< e15 e11)))
(let ((e76 (= e14 v2)))
(let ((e77 (= e13 e14)))
(let ((e78 (> e19 e16)))
(let ((e79 (>= e5 e11)))
(let ((e80 (<= v2 e8)))
(let ((e81 (distinct v1 e21)))
(let ((e82 (distinct e17 e11)))
(let ((e83 (>= v2 e9)))
(let ((e84 (>= e21 v2)))
(let ((e85 (> e8 e8)))
(let ((e86 (<= v0 e18)))
(let ((e87 (< e11 e17)))
(let ((e88 (<= e15 e19)))
(let ((e89 (= e20 e6)))
(let ((e90 (< e12 e16)))
(let ((e91 (< e17 v0)))
(let ((e92 (> v0 e17)))
(let ((e93 (<= e9 e19)))
(let ((e94 (> v2 e20)))
(let ((e95 (> e9 e11)))
(let ((e96 (<= e6 e5)))
(let ((e97 (< v1 e20)))
(let ((e98 (= e16 e15)))
(let ((e99 (= v2 v1)))
(let ((e100 (= e19 e11)))
(let ((e101 (= v0 e16)))
(let ((e102 (> v2 e11)))
(let ((e103 (distinct e20 e19)))
(let ((e104 (< e11 e8)))
(let ((e105 (< e7 e13)))
(let ((e106 (=> e86 e76)))
(let ((e107 (ite e28 e42 e55)))
(let ((e108 (ite e38 e34 e44)))
(let ((e109 (=> e39 e105)))
(let ((e110 (not e95)))
(let ((e111 (or e23 e100)))
(let ((e112 (not e41)))
(let ((e113 (xor e74 e47)))
(let ((e114 (= e89 e43)))
(let ((e115 (xor e31 e111)))
(let ((e116 (ite e80 e65 e113)))
(let ((e117 (and e22 e78)))
(let ((e118 (= e91 e71)))
(let ((e119 (and e114 e90)))
(let ((e120 (ite e51 e35 e59)))
(let ((e121 (not e30)))
(let ((e122 (ite e77 e108 e112)))
(let ((e123 (not e68)))
(let ((e124 (ite e122 e67 e62)))
(let ((e125 (=> e40 e33)))
(let ((e126 (not e120)))
(let ((e127 (not e99)))
(let ((e128 (ite e49 e73 e50)))
(let ((e129 (or e101 e61)))
(let ((e130 (not e115)))
(let ((e131 (=> e121 e117)))
(let ((e132 (= e72 e25)))
(let ((e133 (and e88 e46)))
(let ((e134 (xor e106 e29)))
(let ((e135 (= e103 e52)))
(let ((e136 (and e66 e79)))
(let ((e137 (ite e82 e85 e128)))
(let ((e138 (= e45 e109)))
(let ((e139 (or e87 e135)))
(let ((e140 (= e48 e94)))
(let ((e141 (xor e92 e92)))
(let ((e142 (ite e36 e97 e129)))
(let ((e143 (ite e83 e119 e27)))
(let ((e144 (=> e93 e84)))
(let ((e145 (and e142 e123)))
(let ((e146 (not e116)))
(let ((e147 (and e124 e104)))
(let ((e148 (xor e24 e60)))
(let ((e149 (= e125 e26)))
(let ((e150 (not e110)))
(let ((e151 (=> e118 e145)))
(let ((e152 (xor e130 e144)))
(let ((e153 (xor e37 e148)))
(let ((e154 (xor e107 e102)))
(let ((e155 (=> e147 e57)))
(let ((e156 (xor e53 e132)))
(let ((e157 (not e151)))
(let ((e158 (ite e134 e156 e96)))
(let ((e159 (=> e146 e32)))
(let ((e160 (xor e98 e98)))
(let ((e161 (= e64 e140)))
(let ((e162 (= e127 e158)))
(let ((e163 (xor e133 e54)))
(let ((e164 (= e69 e160)))
(let ((e165 (= e136 e56)))
(let ((e166 (=> e150 e163)))
(let ((e167 (=> e137 e138)))
(let ((e168 (ite e161 e166 e155)))
(let ((e169 (ite e139 e139 e168)))
(let ((e170 (ite e143 e152 e162)))
(let ((e171 (ite e170 e141 e169)))
(let ((e172 (=> e164 e58)))
(let ((e173 (or e154 e70)))
(let ((e174 (= e153 e75)))
(let ((e175 (and e159 e63)))
(let ((e176 (=> e157 e149)))
(let ((e177 (= e126 e175)))
(let ((e178 (xor e176 e131)))
(let ((e179 (or e81 e177)))
(let ((e180 (ite e173 e171 e172)))
(let ((e181 (= e167 e180)))
(let ((e182 (and e179 e181)))
(let ((e183 (or e178 e178)))
(let ((e184 (=> e174 e182)))
(let ((e185 (=> e165 e165)))
(let ((e186 (not e184)))
(let ((e187 (and e185 e183)))
(let ((e188 (not e186)))
(let ((e189 (xor e188 e188)))
(let ((e190 (xor e189 e189)))
(let ((e191 (or e190 e190)))
(let ((e192 (not e187)))
(let ((e193 (and e191 e192)))
e193
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
